l:IdLnk, da:fpf(Knd; k.Type), tg:Id.
(fpf-dom(id-deq; tg; es-dt(l; da)))  (fpf-dom(Kind-deq; rcv(l,tg); da)) 

latex

Definitions

IdLnk, t  T, Knd, x. t(x), x:A. B(x), fpf(A; a.B(a)), Id, top, fpf-domain(f), rcv(l,tg), (x  l), b, A c B, P  Q, x:A. B(x), if b then t else f fi , outl(x), isl(x), , prop{i:l}, P  Q, P  Q, P  Q, , Unit, tag(k), lnk(k), eq_lnk(a; b), isrcv(k), compose-fpf(a; b; f), es-dt(l; da), Kind-deq, id-deq, fpf-dom(eq; x; f), False, True, ff, A, b, guard(T), sq_type(T), P  Q, T

Lemmas

squash wf, bool cases, bool sq, bfalse wf, eqtt to assert, eqff to assert, iff transitivity, assert of bnot, not functionality wrt iff, assert-eq-lnk, bool wf, bnot wf, not wf, true wf, false wf, member-fpf-domain, fpf-dom wf, es-dt wf, id-deq wf, Kind-deq wf, iff functionality wrt iff, compose-fpf-dom, isrcv wf, ifthenelse wf, eq lnk wf, lnk wf, tagof wf, unit wf, it wf, assert wf, l member wf, rcv wf, fpf-domain wf, fpf-trivial-subtype-top, Id wf, fpf wf, Knd wf, IdLnk wf